\begin{tabbing}
next{-}world{-}state($D$;$i$;$s$;$k$;$v$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$<$shift{-}state($\lambda$$x$.d{-}m($D$; $i$).ef($k$,$x$,read{-}state($s$),$v$)?$s$($x$))\+
\\[0ex], doact($k$;$v$)
\\[0ex], filter($\lambda$$m$.source(mlnk($m$)) = $i$;d{-}m($D$; $i$).sends($k$,read{-}state($s$),$v$))$>$
\-
\end{tabbing}